#include "StepByStep.h"

#ifdef CHANGENAME
//       Predication -- Name of Para
//                       ||
//                       VV
//      ActKnowledge    Name Para Of ActK
//                       ||
//                       VV
//      PC Of Action -- Name of Para
void ChangeNameParaOfAction(ActKnowledge *ActK, PredKnowledge *Pd)
{
  PredKnowledge *PC;
  TypedList     *P1, *Para;
  int            i, j, Num, Num1;

  Num = NumParaOfAct(ActK->ActNo);
  Num1 = NumParaOfPred(Pd->PredNo);

  Para = Pd->Para;
  P1 = ActK->Para;
  for (i = 0; i < Num; i++,P1++) {
    j = P1->VList.ParaIdx;
    if (j < Num1) strcpy(P1->VList.Name, (Para+j)->VList.Name);
  }

  for (PC = ActK->PC; PC != NULL; PC = PC->next) {
    P1 = PC->Para;
    Num1 = NumParaOfPred(PC->PredNo);
    for (i = 0; i < Num1; i++,P1++) {
      j = P1->VList.ParaIdx;
      if (0<=j && j<Num) strcpy(P1->VList.Name, (ActK->Para+j)->VList.Name);
    }
  }
}
#endif

//       Predication -- Para
//                       ||
//                       VV
//      ActKnowledge    Para Of ActK
Status ChangeParaOfActionByPred(ActKnowledge *ActK, PredKnowledge *Pd)
{
  TypedList *P1, *P2;
  Status    Change;
  int       i, Idx1, Idx2, Num1, Num2;

  Num1 = NumParaOfPred(Pd->PredNo) + Pd->NumEP;
  Num2 = NumParaOfAct(ActK->ActNo);

  Change = FALSE;
  P1 = ActK->Para;
  for (i = 0; i < Num2; i++,P1++) {
    Idx2 = P1->VList.ParaIdx;
    if (Idx2 >= Num1) continue;

    P2 = Pd->Para + Idx2;
    if (P1->VList.NumValue == 1) {
       Idx1 = P1->VList.List->Idx;
       if (!CheckValueList(Idx1, &(P2->VList))) return ERROR;
       continue;
    }

    if (!EqualTwoVLists(&(P1->VList), &(P2->VList))) {
       CopyValueList(&(P1->VList), &(P2->VList));
       Change = TRUE;
    }
  }

  return Change;
}

//      ActKnowledge -- Para
//                       ||
//                       VV
//       Predication    Para Of PC
Bool ChangeOnePCByAction(PredKnowledge *PC, TypedList *Para)
{
  TypedList *P1, *P2;
  Bool       Change;
  int        i, Idx, Num;

  Change = FALSE;
  P1 = PC->Para;
  PC->NumNonValue = Num = NumParaOfPred(PC->PredNo);
  for (i = 0; i < Num; i++,P1++) {
    Idx = P1->VList.ParaIdx;
    P2 = Para + Idx;
    if (!IsConstant(Idx) && !EqualTwoVLists(&(P1->VList), &(P2->VList))) {
       CopyValueList(&(P1->VList), &(P2->VList));
       Change = TRUE;
    }

    if (P1->VList.NumValue > 0) PC->NumNonValue--;
  }

  return Change;
}

//      ActKnowledge -- Para of ActK
//                       ^^
//                       ||
//       Predication    Para Of PC
Bool ChangeParaOfActionByPC(ActKnowledge *ActK, PredKnowledge *PC)
{
  TypedList *P1, *P2;
  Bool       Change;
  int        i, Num;

  if (ActK == NULL) return FALSE;

  P2 = PC->Para;
  Change = FALSE;
  Num = NumParaOfPred(PC->PredNo);
  for (i = 0; i < Num; i++,P2++) {
    if (IsConstant(P2->VList.ParaIdx)) continue;

    P1 = ActK->Para + P2->VList.ParaIdx;
    if (!EqualTwoVLists(&(P1->VList), &(P2->VList))) {
       CopyValueList(&(P1->VList), &(P2->VList));
       Change = TRUE;
    }
  }

  P2 = ActK->Para;
  Num = NumParaOfAct(ActK->ActNo);
  for (i = 0; i < Num; i++,P2++)
    if (P2->VList.NumValue == 0) break;

  return Change;
}

Bool FindOneCurrentFact(PredKnowledge *Pred, Bool *Change)
{
  TypedList *Pt1;
  TokenList *Pt2, *Pt3, *Fact;
  PredFact  *FT;
  Bool      Modify;
  int       PNo;

  PNo = Pred->PredNo;
  if (State[PNo].Left < 1) return FALSE;

  if (NumParaOfPred(PNo) == 0) return TRUE;

  Fact = NULL;
  for (FT = State[PNo].List; FT != NULL; FT = FT->next) {
    Pt1 = Pred->Para;

    for (Pt2 = FT->Para; Pt2 != NULL; Pt1++,Pt2=Pt2->next)
      if (!CheckValueList(Pt2->VList.List->Idx, &(Pt1->VList))) break;

    if (Pt2 == NULL) {
       if (Fact == NULL) Fact = CopyTokenList(FT->Para);
       else {
              Pt3 = Fact;
              for (Pt2 = FT->Para; Pt2 != NULL; Pt2=Pt2->next,Pt3=Pt3->next)
                InsertOneValueIntoValueList(Pt2->VList.List->Idx, &(Pt3->VList));
       }
    }
  }

  if (Fact == NULL) return FALSE;

  Modify = FALSE;
  Pt1 = Pred->Para;
  for (Pt2 = Fact; Pt2 != NULL; Pt1++,Pt2=Pt2->next)
    if (!EqualTwoVLists(&(Pt1->VList), &(Pt2->VList))) {
       CopyValueList(&(Pt1->VList), &(Pt2->VList));
       Modify = TRUE;
    }

  if (Modify) {
     ModifyAllParentsByPC(Pred);
     *Change = TRUE;
  }

  FreeTokenList(Fact);

  return TRUE;
}

void InsertOrCombinePCParaNode(PCParaLink **PL, Bool Fact, TokenList *Para)
{
  PCParaLink *PL1;

  PL1 = (PCParaLink *) calloc(1, sizeof(PCParaLink));
  PL1->Para = CopyTokenList(Para);
  PL1->Fact = Fact;
  PL1->next = *PL;
  *PL = PL1;
}

Bool PCMatchsEffect(PredKnowledge *PC, PENode *PE)
{
  TypedList *Pt1;
  TokenList *Pt2;
  Bool       Matched;

  Pt1 = PC->Para;
  Pt2 = PE->Pred;
  Matched = (PC->Type==PE->Type && PC->PredNo==Pt2->VList.ParaIdx);
  for (Pt2 = Pt2->next; Matched && Pt2!=NULL; Pt1++,Pt2=Pt2->next) {
    if (Pt1->VList.NumValue == 0) continue;

    if (Pt1->VList.NumValue == 1) {
       if (Pt2->VList.NumValue == 1)
          Matched = (Pt1->VList.List->Idx==Pt2->VList.List->Idx);
       else
          Matched = CheckValueList(Pt1->VList.List->Idx, &(Pt2->VList));
    }
    else if (Pt2->VList.NumValue == 1)
            Matched = CheckValueList(Pt2->VList.List->Idx, &(Pt1->VList));
         else
            Matched = EqualTwoVLists(&(Pt2->VList), &(Pt1->VList));
  }

  return Matched;
}

// Find the corresponding fact or noconfirm fact
PCParaLink* GetParaWithFactNFFact(Bool Used, NCAction *Tail, PredKnowledge *PC)
{
  ActKnowledge *ActK;
  PCParaLink   *PL;
  TypedList    *Pt1;
  TokenList    *Pt2;
  PredFact     *Fact;
  NCAction     *nAct;
  PENode       *PE;

  PL = NULL;
  for (nAct = Tail; nAct != NULL; nAct = nAct->prev) {
    for (PE = nAct->Pred->CEffect; PE != NULL; PE = PE->next)
      if ((Used || !PE->Delete) && PCMatchsEffect(PC, PE))
         InsertOrCombinePCParaNode(&PL, FALSE, PE->Pred->next);

    for (ActK = nAct->Pred->Act; ActK != NULL; ActK = ActK->next)
      for (PE = ActK->Effect; PE != NULL; PE = PE->next)
        if ((Used || !PE->Delete) && PCMatchsEffect(PC, PE))
           InsertOrCombinePCParaNode(&PL, FALSE, PE->Pred->next);
  }

  if (State[PC->PredNo].Left>0 && (PC->Fact || PL==NULL))
     for (Fact = State[PC->PredNo].List; Fact!=NULL; Fact = Fact->next) {
       if (Fact->Finish) continue;

       Pt1 = PC->Para;
       for (Pt2 = Fact->Para; Pt2 != NULL; Pt1++,Pt2=Pt2->next)
         if (Pt1->VList.NumValue != 0 &&
             !CheckValueList(Pt2->VList.List->Idx, &(Pt1->VList))) break;

       if (Pt2 == NULL) InsertOrCombinePCParaNode(&PL, TRUE, Fact->Para);
     }

  return PL;
}

PredKnowledge* CopyOnePC(PredKnowledge *PC)
{
  PredKnowledge *PC1;

  PC1 = (PredKnowledge *) calloc(1, sizeof(PredKnowledge));

  PC1->SAT = PC->SAT;
  PC1->Fact = PC->Fact;
  PC1->Type = PC->Type;
  PC1->Index = PC->Index;
  PC1->Level = PC->Level;
  PC1->Height = PC->Height;
  PC1->PredNo = PC->PredNo;
  PC1->NumEP = PC->NumEP;
  PC1->Character = PC->Character;
  PC1->NumNonValue = PC->NumNonValue;

  PC1->Para = CopyTypedArray(NumParaOfPred(PC->PredNo)+PC->NumEP, PC->Para);

  return PC1;
}

ActKnowledge* CopyActKnowledge(ActKnowledge *ActK, PredKnowledge *Parent)
{
  PredKnowledge *PC, *PC1, *PC2;
  ActKnowledge  *ActK1;
  PENode        *PE, *PE1, *PE2;

  ActK1 = (ActKnowledge *) calloc(1, sizeof(ActKnowledge));

  ActK1->ActNo = ActK->ActNo;
  ActK1->Type = ActK->Type;
  ActK1->Index = ActK->Index;
  ActK1->Height = ActK->Height;

  ActK1->Parent = Parent;
  ActK1->Para = CopyTypedArray(NumParaOfAct(ActK->ActNo), ActK->Para);

  for (PC = ActK->PC; PC != NULL; PC = PC->next) {
    PC2 = CopyOnePC(PC);

    PC2->PAct = ActK1;
    PC2->Parent = Parent;  PC2->Level = Parent->Level + 2;

    if (ActK1->PC == NULL) ActK1->PC = PC2;
    else PC1->next = PC2;

    PC1 = PC2;
  }

  for (PE = ActK->Effect; PE != NULL; PE = PE->next) {
    PE2 = (PENode *) calloc(1, sizeof(PENode));
    PE2->Type = PE->Type;
    PE2->Delete = PE->Delete;
    PE2->Pred = CopyTokenList(PE->Pred);

    if (ActK1->Effect == NULL) ActK1->Effect = PE2;
    else PE1->next = PE2;
    PE1 = PE2;
  }

#ifdef WHEN_CLAUSE
  for (PE = ActK->CondEffect; PE != NULL; PE = PE->next) {
    PE2 = CopyWhenClause(PE);

    if (ActK1->CondEffect == NULL) ActK1->CondEffect = PE2;
    else PE1->next = PE2;

    PE1 = PE2;
  }
#endif

  return ActK1;
}

void InstanceEffectOfAction(ActKnowledge *ActK)
{
  PENode *PE;
#ifdef WHEN_CLAUSE
  PENode *PE1;
#endif
  int    Num;

  Num = NumParaOfAct(ActK->ActNo);

  for (PE = ActK->Effect; PE != NULL; PE = PE->next)
    InstanceTokenListByTypedList(PE->Pred, Num, ActK->Para);

#ifdef WHEN_CLAUSE
  for (PE = ActK->CondEffect; PE != NULL; PE = PE->next) {
    InstanceTokenListByTypedList(PE->sons->Pred, Num, ActK->Para);

    for (PE1 = PE->Effect; PE1 != NULL; PE1 = PE1->next)
      InstanceTokenListByTypedList(PE1->Pred, Num, ActK->Para);
  }
#endif
}

int GetNumberOfNonValue(PredKnowledge *PC, int *Para)
{
  TypedList *Pt;
  int        i, k, Num;

  Pt = PC->Para;
  Num = NumParaOfPred(PC->PredNo);
  for (i=k=0; i < Num; i++,Pt++)
    if (Pt->VList.NumValue==0 && Para[Pt->VList.ParaIdx]==NOFOUND)
       k++;

  return k;
}

// Sort PCs Of Action By Equal-Pred and NonValue
void SortPCsOfAction(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1, *PC2, *PC3, *PC4, *PC5;
  TypedList     *Pt;
  Bool           Ok, S1, S2;
  int            F1, F2, PNo, PNo1, PNo2;
  int            i, Num, *Para;
#ifndef TEST
  Bool           Ok1;
#endif

  Num = NumParaOfAct(ActK->ActNo);
  Para = (int *) calloc(Num, sizeof(int));
  for (i = 0; i < Num; i++) Para[i] = NOFOUND;

  PNo = ActK->Parent->PredNo;

  PC = NULL;  PC1 = ActK->PC;
  while (PC1 != NULL) {
    PC2 = NULL;
    PC3 = PC1;

    F1 = GetNumberOfNonValue(PC3, Para);

    PNo1 = PC3->PredNo;
    S1 = (IsEqual(PNo1) || IsClass(PNo1, STATIC));

    PC4 = PC1;
    while (PC4->next != NULL) {
      PC5 = PC4->next;
      F2 = GetNumberOfNonValue(PC5, Para);

      PNo2 = PC5->PredNo;
      S2 = (IsEqual(PNo2) || IsClass(PNo2, STATIC));

#ifdef TEST
      Ok = (PC5->Type==ATOM &&
           (PC3->Type==NOT || (!S1 && S2) || (S1==S2 && 0<=F2 && F2<F1)));
#else
      Ok1 = ((PNo2==PNo && PNo1!=PNo) ||
              (((PNo2!=PNo && PNo1!=PNo) || (PNo2==PNo && PNo1==PNo)) &&
               (0 <= F2 && F2 < F1)));
      Ok = (PC5->Type==ATOM &&
            (PC3->Type==NOT || (!S1 && S2) || (S1==S2 && Ok1)));
#endif
      if (Ok) {
         PC2 = PC4;  PC3 = PC5;
         F1 = F2;    PNo1 = PNo2;   S1 = S2;
      }

      PC4 = PC5;
    }

    if (PC2 != NULL) PC2->next = PC3->next;
    else PC1 = PC1->next;

    if (PC == NULL) ActK->PC = PC3;
    else PC->next = PC3;

    Pt = PC3->Para;
    Num = NumParaOfPred(PC3->PredNo);
    for (i = 0; i < Num; i++,Pt++)
      if (Pt->VList.NumValue == 0) Para[Pt->VList.ParaIdx]++;

    PC = PC3;  PC->next = NULL;
  }

  free(Para);
}

// The PCs of Action conflict with its all Parents
Bool ExistPCLoop(PredKnowledge *PC)
{
  PredKnowledge *PC1;
  TypedList     *P1, *P2;
  Bool           Exist;
  int            i, Num;

  Num = NumParaOfPred(PC->PredNo);
  for (PC1 = PC->Parent; PC1 != NULL; PC1 = PC1->Parent) {
    if (PC->Expand != PC1->Expand ||
        PC->Type != PC1->Type || PC->PredNo != PC1->PredNo) continue;

    Exist = TRUE;
    P1 = PC->Para;   P2 = PC1->Para;
    for (i = 0; Exist && i < Num; i++,P1++,P2++)
      if (P1->VList.NumValue > 0) Exist = ValueListInValueList(&(P1->VList), &(P2->VList));
      else if (P2->VList.NumValue > 0) Exist = FALSE;
      else Exist = IsSame(P1->VList.Name, P2->VList.Name);

    if (Exist) return TRUE;
  }

  return FALSE;
}

// Instance all PCs of New Action (ActK)
// Handle Equal Pred or Static Pred In PC Of Action
Bool HandlePCsOfNewAction(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1, *PC2;
  Bool           Ok, Check;

  PC = NULL;
  for (PC1 = ActK->PC; PC1 != NULL; PC1 = PC2) {
    PC2 = PC1->next;

    Check = FALSE;
    if (PC1->NumNonValue == 0) {
       if (IsEqual(PC1->PredNo)) {
          Ok = ((PC1->Para)->VList.List->Idx==(PC1->Para+1)->VList.List->Idx);
          Check = TRUE;
       }
       else if (IsClass(PC1->PredNo, STATIC)) {
               Ok = FindOneCurrentFact(PC1, &Ok);
               Check = TRUE;
            }
    }

    if (Check) {
       if (PC1->Type == NOT) Ok = !Ok;

       if (!Ok) return FALSE;

       if (PC == NULL) ActK->PC = PC2;
       else PC->next = PC2;

       FreePredKnowledge(PC1);

       continue;
    }

    if (ExistPCLoop(PC1)) return FALSE;

    PC = PC1;
  }

  for (PC = ActK->PC; PC != NULL; PC = PC->next) // Check all PCs conflict
    if (!PC->Fact)
       for (PC1 = ActK->PC; PC1 != NULL; PC1 = PC1->next)  // PC --> (not PC1)
         if (PC1!=PC && CheckDomainLawForPreds(Law0, ATOM, PC, NOT, PC1))
            return FALSE;

  return TRUE;
}

void GetValueOfType(ValueList *Vlist, char *TypeName)
{
  TypedList *Pt;
  VList     *VL1, *VL2;
  int        i, Num;

  Num = 0;   VL1 = NULL;

  Pt = Constants;
  for (i = 0; i < NumConstant; i++,Pt++)
    if (TypeInListOfType(TypeName, Pt->Type)) {
       VL2 = (VList *) calloc(1, sizeof(VList));
       VL2->Idx = i + CONSTANT;

       if (VL1 == NULL) Vlist->List = VL2;
       else VL1->next = VL2;

       Num++;    VL1 = VL2;
    }

  Pt = Objects;
  for (i = 0; i < NumObject; i++,Pt++)
    if (TypeInListOfType(TypeName, Pt->Type)) {
       VL2 = (VList *) calloc(1, sizeof(VList));
       VL2->Idx = i;

       if (VL1 == NULL) Vlist->List = VL2;
       else VL1->next = VL2;

       Num++;    VL1 = VL2;
    }

  Vlist->NumValue = Num;

#ifdef TEST
  fprintf(Output, "\n%s - ", TypeName);
  for (VL1 = Vlist->List; VL1 != NULL; VL1 = VL1->next)
    fprintf(Output, "%d, ", VL1->Idx);
  fprintf(Output, "\n");
#endif
}

Bool CheckPCSOfAction(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1;
  Bool           Ok;

  PC1 = NULL;
  for (PC = ActK->PC; PC != NULL; PC1=PC,PC=PC->next) {
    ChangeOnePCByAction(PC, ActK->Para);

    if (PC->NumNonValue > 0) continue;

    if (IsEqual(PC->PredNo)) {
       Ok = ((PC->Para)->VList.List->Idx==(PC->Para+1)->VList.List->Idx);
       if (PC->Type == NOT) Ok = !Ok;

       if (!Ok) break;

       if (PC1 == NULL) ActK->PC = PC->next;
       else PC1->next = PC->next;

       FreeTypedArray(NumParaOfPred(PC->PredNo), PC->Para);
       free(PC);

       PC = PC1;
    }

    if (ExistPCLoop(PC)) break;
  }

  if (PC == NULL) {
     InstanceEffectOfAction(ActK);
     SortPCsOfAction(ActK);
  }

  return (PC == NULL);
}

int HandleEqualPred(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1, *PC2;
  ActKnowledge  *ActK1;
  VList         *Pt1, *Pt2;
  int           i, Idx, Num, Num1;

  PC = ActK->PC;
  while (PC!=NULL && !IsEqual(PC->PredNo)) PC = PC->next;

  if (PC == NULL) return 1;

  Num = 1;
  ChangeOnePCByAction(PC, ActK->Para);
  Num1 = PC->Para[0].VList.NumValue;

  if (Num1 > 1 && PC->Para[1].VList.NumValue > 1) {
     Num = Num1;
     Pt1 = PC->Para[0].VList.List;
     PC->Para[0].VList.NumValue = 1;
     for (i = 1; i < Num; i++) {
       Pt2 = Pt1->next;
       Pt1->next = NULL;

       ActK1 = CopyActKnowledge(ActK, ActK->Parent);
       InsertActKnowledge(AFTER, ActK, ActK1);

       free(Pt1);
       PC->Para[0].VList.List = Pt1 = Pt2;
     }
  }

//PrintPredication(20, ActK->Parent);  fprintf(Output, "\n");
  ActK1 = ActK;
  for (i = 0; i < Num; i++,ActK1=ActK1->next) {
    PC1 = NULL;  PC2 = ActK1->PC;
    while (!IsEqual(PC2->PredNo)) PC1=PC2, PC2=PC2->next;

    Num1 = (PC2->Para[0].VList.NumValue==1 ? 0 : 1);

    Idx = (PC2->Para+Num1)->VList.List->Idx;

    DeleteOneValueFromValueList(Idx, &((PC2->Para+1-Num1)->VList));

    ChangeParaOfActionByPC(ActK1, PC2);

    if (PC1 == NULL) ActK1->PC = PC2->next;
    else PC1->next = PC2->next;

    FreePredKnowledge(PC2);  free(PC2);
  }

  return Num;
}

ActKnowledge *InstantActionForTyping(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1;
  ActKnowledge  *ActK1;
  TypedList     *P1, *P2;
  VList         *Pt1;
  Bool           In, Delete;
  int            i, j, Num, Num1;

  P1 = ActK->Para;
  Num = NumParaOfAct(ActK->ActNo);
  for (i = 0; i < Num; i++,P1++)
    if (P1->VList.NumValue == 0) GetValueOfType(&(P1->VList), P1->Type->Name);

//PrintActKnowledge(12, ActK);fprintf(Output, "\n");

  Num = (IsType(ActK->Type, Equal) ? HandleEqualPred(ActK) : 1);

//PrintPredication(20, ActK->Parent);  fprintf(Output, "\n");

  ActK1 = ActK;
  for (i = 0; i < Num; i++, ActK1=ActK1->next) {
    PC = ActK1->PC;
    while (PC != NULL) {
      ChangeOnePCByAction(PC, ActK1->Para);

      Delete = FALSE;
      Num1 = NumParaOfPred(PC->PredNo);
      for (PC1 = PC->Parent; PC1 != NULL; PC1 = PC1->Parent) {
        if (PC->Type!=PC1->Type || PC->PredNo!=PC1->PredNo) continue;

        In = TRUE;
        P1 = PC->Para;    P2 = PC1->Para;
        for (j = 0; In && j < Num1; j++,P1++,P2++)
          In = ValueListInValueList(&(P2->VList), &(P1->VList));

        if (In) {
           P1 = PC->Para;   P2 = PC1->Para;
           for (j = 0; j < Num1; j++,P1++,P2++)
             if (P2->VList.NumValue < P1->VList.NumValue) {
                Delete = TRUE;
                for (Pt1 = P2->VList.List; Pt1 != NULL; Pt1 = Pt1->next)
                  DeleteOneValueFromValueList(Pt1->Idx, &(P1->VList));
             }
        }
      }

      if (!Delete) PC = PC->next;
      else {
             ChangeParaOfActionByPC(ActK1, PC);
             PC = ActK1->PC;
      }
    }

    InstanceEffectOfAction(ActK1);
  }

  return ActK;
}

Bool PredIsNoConfirmFact(PredKnowledge *Pred, TokenList *Pt)
{
  TypedList *Pt1;
  Bool       Ok;

  Pt1 = Pred->Para;
  Ok = (Pred->PredNo == Pt->VList.ParaIdx);
  for (Pt = Pt->next; Ok && Pt!=NULL; Pt1++,Pt=Pt->next)
    if (Pt1->VList.NumValue == 0) Ok = FALSE;
    else if (Pt1->VList.NumValue == 1)
            Ok = CheckValueList(Pt1->VList.List->Idx, &(Pt->VList));
         else if (Pt->VList.NumValue == 1)
                 Ok = CheckValueList(Pt->VList.List->Idx, &(Pt1->VList));
              else
                 Ok = ValueListInValueList(&(Pt1->VList), &(Pt->VList));

  return Ok;
}

Bool FindOneNoConfirmFact(PredKnowledge *PC, NCAction *Tail)
{
  ActKnowledge *ActK;
  NCAction     *nAct;
  PENode       *PE;

  for (nAct = NCA; nAct != Tail; nAct = nAct->next) {
//PrintPredication(12, nAct->Pred); fprintf(Output, "\n");
    for (PE = nAct->Pred->CEffect; PE != NULL; PE = PE->next)
      if (!PE->Delete && PE->Type==PC->Type &&
          PredIsNoConfirmFact(PC, PE->Pred))
         return TRUE;

    for (ActK = nAct->Pred->Act; ActK != NULL; ActK = ActK->next)
      for (PE = ActK->Effect; PE != NULL; PE = PE->next)
        if (!PE->Delete && PE->Type==PC->Type &&
            PredIsNoConfirmFact(PC, PE->Pred))
           return TRUE;
  }

  return FALSE;
}

// Change Para of all PCs of the action
Bool ChangeParaOfAllPCOfAction(ActKnowledge *ActK)
{
  PredKnowledge *PC;
  ActKnowledge  *ActK1, *ActK2;
  Bool           Ok, Ok1, UComplete;
  int            HAct, Acts;

  for (PC = ActK->PC; PC != NULL; PC = PC->next) {
    if (!ChangeOnePCByAction(PC, ActK->Para)) continue;

    if (ExistPCLoop(PC)) return ERROR;

    Ok1 = (PC->Act != NULL);

    HAct = Acts = -1;
    if (Ok1) HAct = Acts = MAX_HEIGHT;

    UComplete = (PC->Act != NULL);
    for (ActK1 = PC->Act; ActK1 != NULL; ActK1 = ActK2) {
      ActK2 = ActK1->next;

      Ok = ChangeParaOfActionByPred(ActK1, PC);

      if (Ok == ERROR) { DeleteActKnowledge(ActK1); continue; }

      if (Ok == TRUE) {
         Ok = ChangeParaOfAllPCOfAction(ActK1);
         if (Ok == ERROR) { DeleteActKnowledge(ActK1); continue; }
      }

      if (HAct > ActK1->Height) HAct = ActK1->Height;
      if (Acts > ActK1->Acts) Acts = ActK1->Acts;
      UComplete = UComplete && ActK1->UComplete;
    }

    if (Ok1 && PC->Act==NULL) return ERROR;

    PC->Height = HAct + 1;   PC->Acts = Acts + 1;

    if (!UComplete || PC->Act == NULL) PC->UComplete = FALSE;
#ifdef DFS
    else ModifyKnowledgeTree(MAX_HEIGHT, PC);
#else
    else ModifyKnowledgeTreeByBFS(PC);
#endif
  }

  return TRUE;
}

/*void InstanceCPCOfPred(PredKnowledge *Pred)
{
  PredKnowledge *CPC;
  TypedList     *Para, *Para1;
  int           i, j, Num;

  for (CPC = Pred->CPC; CPC != NULL; CPC = CPC->next) {
    Num = NumParaOfPred(CPC->PredNo);
    Para = CPC->Para;
    for (i = 0; i < Num; i++,Para++) {
      j = Para->VList.ParaIdx;
      if (!IsConstant(j)) {
         Para1 = Pred->Para + j;
         if (Para->VList.NumValue != Para1->VList.NumValue)
            CopyValueList(&(Para->VList), &(Para1->VList));
      }
    }
  }
}*/

Bool ModifyParaOfPredByActions(PredKnowledge *Pred)
{
  ActKnowledge *ActK;
  TypedList    *P1, *Para;
  PENode       *PE;
  Bool         Ok, Change;
  int          i, j, Num, Num1;

  Num = NumParaOfPred(Pred->PredNo) + Pred->NumEP;
  if (Num == 0) return FALSE;

//PrintPredication(12, Pred); fprintf(Output, "\n");
  Para = (TypedList *) calloc(Num, sizeof(TypedList));

  for (ActK = Pred->Act; ActK != NULL; ActK = ActK->next) {
    if (ActK->UComplete) continue;

    P1 = ActK->Para;
    Num1 = NumParaOfAct(ActK->ActNo);
    for (i = 0; i < Num1; i++,P1++) {
      j = P1->VList.ParaIdx;
      if (j < Num) MergeTwoVLists(&((Para+j)->VList), &(P1->VList));
    }
  }

//PrintPredication(12, Pred); fprintf(Output, "\n");
  Change = CopyTwoTypedLists(Num, Pred->Para, Para);

  FreeTypedArray(Num, Para);

//InstanceCPCOfPred(Pred);

  // Instance all common effects Of Pred
  Num = NumParaOfPred(Pred->PredNo) + Pred->NumEP;
  for (PE = Pred->CEffect; PE != NULL; PE = PE->next)
    InstanceTokenListByTypedList(PE->Pred, Num, Pred->Para);

  Ok = TRUE;
  ActK = Pred->PAct;
  if (Change && ChangeParaOfActionByPC(ActK, Pred)) {
     Ok = ChangeParaOfAllPCOfAction(ActK);
     InstanceEffectOfAction(ActK);
  }

  return Ok;
}

Bool PCObsOtherPC(PredKnowledge *PC, PredKnowledge *PAct, ActKnowledge *ActK)
{
  TypedList *P1, *Para;
  Bool       Ok;
  int        i, Num, Num1;

  Num = NumParaOfPred(PAct->PredNo);
  Para = CopyTypedArray(Num, PAct->Para);

  Num1 = NumParaOfAct(ActK->ActNo);
  P1 = ActK->Para;
  for (i = 0; i < Num1; i++,P1++)
    if (P1->VList.ParaIdx < Num)
       CopyValueList(&((Para+P1->VList.ParaIdx)->VList), &(P1->VList));

  P1 = PAct->Para;
  PAct->Para = Para;

  // PC --> (not PAct)
  Ok = CheckDomainLawForPreds(Law0, ATOM, PC, NOT, PAct);

  FreeTypedArray(Num, Para);
  PAct->Para = P1;

  return Ok;
}

Bool CheckAllPCsOfAction(ActKnowledge *ActK)
{
  PredKnowledge *PC, *PC1;
  ActKnowledge  *ActK1, *ActK2;
  Bool           Change, UComplete;
  PENode *PE;

  for (PC = ActK->PC; PC != NULL; PC = PC->next) {
    if (PC->Act != NULL) continue;

    for (PC1 = ActK->PC; PC1 != NULL; PC1 = PC1->next) {
      if (PC == PC1) continue;

      Change = FALSE;
      UComplete = TRUE;
      for (ActK1 = PC1->Act; ActK1 != NULL; ActK1 = ActK2) {
        ActK2 = ActK1->next;
        if (ActK1->UComplete) continue;

        for (PE = ActK1->Effect; PE != NULL; PE = PE->next)
          if (NOTPredInOneEffect(PC, PE)) break;

        if (PE != NULL && PCObsOtherPC(PC, PC1, ActK1)) {
           DeleteActKnowledge(ActK1);
           Change = TRUE;
        }
        else UComplete = FALSE;
      }

      if (Change) {
         if (PC1->Act == NULL) return FALSE;

         PC1->UComplete = UComplete;
         ModifyParaOfPredByActions(PC1);
      }
    }
  }

  return TRUE;
}

Bool CheckPredKnowledgeTree(PKTree *Pk, PredKnowledge *Pd)
{
  PredKnowledge *PC;
  TypedList     *Pt1, *Pt2;
  TokenList     *Pt3;
  PredFact      *Ft;
  int           i, idx1, idx2, Num, Num1;

  Num = NumParaOfPred(Pd->PredNo);

  PC = Pk->PC;
  if (PC != NULL) {
     Num1 = NumParaOfPred(PC->PredNo);
     Pt1 = PC->Para;
     for (i = 0; i < Num1; Pt1++,i++) {
       idx1 = Pt1->VList.ParaIdx;
       if (!IsConstant(idx1)) {
          if (idx1 >= Num) FreeValueList(&(Pt1->VList));
          else CopyValueList(&(Pt1->VList), &(Pd->Para+idx1)->VList);
       }
     }

//PrintPKTree(Pk);
     if (State[PC->PredNo].Left == 0) return FALSE;

     for (Ft = State[PC->PredNo].List; Ft!=NULL; Ft = Ft->next) {
       if (Ft->Finish) continue;

       Pt1 = PC->Para;
       for (Pt3 = Ft->Para; Pt3 != NULL; Pt1++,Pt3=Pt3->next)
         if (Pt1->VList.NumValue != 0 &&
            !CheckValueList(Pt3->VList.List->Idx, &(Pt1->VList))) break;

       if (Pt3 == NULL) break;
     }

     if (Ft == NULL) return FALSE;
  }

  Pt1 = Pd->Para;  Pt2 = Pk->Pred->Para;
  for (i = 0; i < Num; i++,Pt1++,Pt2++) {
    idx1 = Pt1->VList.ParaIdx;
    idx2 = Pt2->VList.ParaIdx;
    if (IsConstant(idx1)) {
       if (IsConstant(idx2) && idx1 != idx2) break;
    }
    else if (IsConstant(idx2) ||
             (Typing && !TypeInListOfType(Pt2->Type->Name, Pt1->Type)))
            break;
  }

  return (i >= Num);
}

void CopyListOfCEffect(PredKnowledge *Pd, PredKnowledge *Pred)
{
  PENode *PE, *PE1;

  Pd->CEffect = NULL;
  for (PE = Pred->CEffect; PE != NULL; PE = PE->next) {
    PE1 = CopyPENode(PE);
    PE1->next = Pd->CEffect;
    Pd->CEffect = PE1;
  }
}
